es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id }, p:({e:E| loc(e) = loc(e1)  Id }Prop).
e2 = first e  e1.p(e)  Prop 

latex

Definitions	b, P  Q, False, A, t  T, x:A. B(x), loc(e), Id, E, x(s), Prop, x. t(x), e[e1,e2).P(e), P & Q, e2 = first e  e1.P(e), ES
Lemmas	event system wf, alle-between1 wf, not wf, es-E wf, Id wf, es-loc wf, es-loc-pred